%
% Copyright (C) Håkan Lindqvist 2006, 2007.
% May be copied freely for educational and personal use. Any other use
% needs my written consent (i.e. no commercial use without my approval).
%
% \begin{verbatim}
% http://en.wikipedia.org/wiki/Discrete_mathematics
% \end{verbatim}

\label{chapter:math}

In the formal aspects of computer security theory, the most common tool
is mathematics. More specifically, set theory is used to a large extent
to express properties between entities in systems and their relations.
This chapter will provide a very basic introduction to the topics set
theory and the closely related field of propositional logic.
All material presented is adapted from the book ``Discrete and Combinatorial
Mathematics''~\cite{grimaldi} and ``Mathematical Logic for Computer
Science''~\cite{logic}.

%The theory presented in this chapter is very fundamental, and any reader
%that feels confident with these topics may skip the entire chapter.

%
\section{Propositional logic}\index{logic!propositional}
Propositional logic, or more correctly propositional calculus, work with
expressions with two possible values: \texttt{true} or \texttt{false}.
That is, each expression has only two possible values. How such
expressions, and the fundamental parts that form them, will be
presented below.

\subsection{Atomic propositions}\index{logic} \index{logic!atomic proposition}
To assign any meaning to a logical expression, all parts of it must have
a defined meaning. The assignment is done through the basic building
blocks called atomic proposition. These are the sentences that can not
be divided into any smaller compositions, and therefore have a fixed
value of \texttt{true} or \texttt{false}. How compositions of atomic
propositions are made is defined in Section~\ref{logic:formulas}. It
describes how to apply rules to build ``formulas'' using operators
presented in the following section

\subsection{Operators} \index{logic!operator}
Any expression in propositional logic can be subjected to an operator
since the expression only represents a value. The operators either
directly affect the value that the expression evaluates to, or take
the value and combine it with another value to form a new expression,
which in turn gives a new value.

The operators that were described were unary and binary, respectively.
Figure~\ref{logic operators} presents relevant operators, in order of
precedence.
%The following table presents the relevant operators, in order of
%precedence:

\begin{figure}[!htpb]
\begin{footnotesize}
\begin{center}
\begin{tabular}{cccc}
  Symbol & Type    & Name & Example \\
  \hline
  $\lnot$ & Unary  & Negate & $\lnot \, expr$           \\
  $\lor$  & Binary & Disjunction & $expr1 \, \lor \, expr2$  \\
  $\land$ & Binary & Conjunction & $expr1 \, \land \, expr2$ \\
  $\to$   & Binary & Implication & $expr1 \, \to \, expr2$   \\
  $\oplus$       & Binary     & Exclusive or & $expr1 \, \oplus \,  expr2$ \\
  $\uparrow$     & Binary & Nor & $expr1 \, \uparrow \, expr2$     \\
  $\downarrow$   & Binary & Nand & $expr1 \, \downarrow \, expr2$   \\
  $\leftrightarrow$  & Binary & Equivalence & $expr1 \, \leftrightarrow \, expr2$
\end{tabular}
\end{center}
\end{footnotesize}

\begin{center}
\caption{Operators in basic propositional logic, shown in order of
precedence \cite{logic}}
\end{center}
\label{logic operators}
\end{figure}

The interpretation of an operator is easily represented with a
truthtable, in which all possible of expression values that the operator
uses and the outcome are presented.


\begin{figure}[!htpb]
\begin{tiny}
\begin{center}
\begin{tabular}{c | c | c | c} \label{logic:interpret}
  Operator & Expression & Resulting value \\
  \hline
  $\lnot$  & True   & False & \\
           & False  & True  & \\

           &        &       & \\
           &        &       & \\

  Operator & Expression one & Expression two & Resulting value \\
  \hline
  $\land$  & True  & True    & True\\
           & True  & False   & False\\
           & False & True    & False\\
           & False & False   & False\\

           &        &       & \\
           &        &       & \\

  Operator & Expression one & Expression two & Resulting value \\
  \hline
  $\lor$  & True  & True    & True\\
          & True  & False   & True\\
          & False & True    & True\\
          & False & False   & False\\

           &        &       & \\
           &        &       & \\

  Operator & Expression one & Expression two & Resulting value \\
  \hline
  $\to$  & True  & True    & True\\
         & True  & False   & False\\
         & False & True    & True\\
         & False & False   & True\\

           &        &       & \\
           &        &       & \\

  Operator & Expression one & Expression two & Resulting value \\
  \hline
  $\oplus$  & True  & True    & False\\
            & True  & False   & True\\
            & False & True    & True\\
            & False & False   & False\\

           &        &       & \\
           &        &       & \\


  Operator & Expression one & Expression two & Resulting value \\
  \hline
  $\uparrow$  & True  & True    & False\\
              & True  & False   & True\\
              & False & True    & True\\
              & False & False   & True\\

           &        &       & \\
           &        &       & \\

  Operator & Expression one & Expression two & Resulting value \\
  \hline
  $\downarrow$  & True  & True    & False\\
                & True  & False   & False\\
                & False & True    & False\\
                & False & False   & True\\

           &        &       & \\
           &        &       & \\

  Operator & Expression one & Expression two & Resulting value \\
  \hline
  $\leftrightarrow$  & True  & True    & True\\
                     & True  & False   & False\\
                     & False & True    & False\\
                     & False & False   & True
\end{tabular}
\end{center}
\end{tiny}

\begin{center}
\caption{Interpretation of logical operators \cite{logic}}
\end{center}
\end{figure}

The $\leftrightarrow$ operator also hints of what is defined as logical
equivalence; two expressions with the same value are considered to be
logically equivalent. That is, one can exchange one for the other in
some larger, nested, expression and the value of that expression does
not change.
The notion of nested, large, expression is the topic of the next
section.

%
\subsection{Formulas}\label{logic:formulas}\index{logic!formula}
In the previous section, the term ``expression'' was used extensively to
provide context for the operators described. In propositional logic
however, the more common term is ``formula.''

A formula is defined as a syntactically correctly formatted set of
operators and identifiers with respect to the following rules, where
$::=$ is syntactic assignment (i.e. what a word can be replaced with,
how to interpret the resulting formula is defined using 
Figure~\ref{logic:interpret}):

\begin{enumerate}
 \item $fml \, ::= \, p$, for any symbol $p$ that represents some value
 \item $fml \, ::= \, \lnot fml$
 \item $fml \, ::= \, fml \, \lor \, fml$
 \item $fml \, ::= \, fml \, \land \, fml$
 \item $fml \, ::= \, fml \, \to \, fml$
 \item $fml \, ::= \, fml \, \leftrightarrow \, fml$
 \item $fml \, ::= \, fml \, \oplus \, fml$
 \item $fml \, ::= \, fml \, \uparrow \, fml$
 \item $fml \, ::= \, fml \, \downarrow \, fml$
\end{enumerate}

The reader should note that several of the rules are mutually recursive.

%
\subsection{Quantifiers}\index{logic!quantifier}
Quantifiers are simple operators that express a count of symbols that
holds some property. The two commonly used quantifiers are ``for all'',
$\forall$, and ``exists'' (at least one), $\exists$. 
How these are used is best illustrated with an example:
\begin{displaymath}
  \forall x ( q \to p )
\end{displaymath}

The above formula is read as: ``for all $x$ for which the expression $q$
implies $p$ is true.``

\begin{displaymath}
  \exists x ( q \to p )
\end{displaymath}

The above formula is read as: ``there exists at least one $x$ for which
the expression $q$ implies $p$ is true.``

\newpage
%
\section{Set theory}\index{set}\index{set theory}
Set theory is a mathematical way of grouping abstract objects, which may
be logical representations of real objects, and describing relations
between them. 

This section will start out with the definition of what a set is, and
then continue with some smaller elaboration on how objects inside a set
may be ordered, forming structures such as a lattice.

%
\subsection{Forming sets}
A set is simply a grouping of several objects, using some criteria for
the grouping. An intuitive set to use as an example is the set of
natural numbers, which can be expressed with the use of logic:

\begin{displaymath}
  N = \left\{ x \, | \, \forall x \, \texttt{such that x is a
  non-negative integer} \right\} = \left\{ 0, 1, 2, \ldots \right\}
\end{displaymath}


%
\subsection{Special properties and operators}
\index{set!properties}
\index{set!operators}
Since a set is an abstract way of grouping objects, some special
characteristics have been associated with them to ensure proper
interpretation. The more fundamental properties and operators
are described below.

\subsubsection{Union}\index{set!union}
A set is a collection of unique objects, that is, if you form a new set
by combining two existing sets which both have some object $x$, only one
$x$ will be present in the new set. Such an action is called a union of
two sets and is expressed here with an example:

\begin{displaymath}
  \left\{1, 2, 3\right\} \cup \left\{1, a, a , b\right\} =
  \left\{1, 2, 3, a, b\right\}
\end{displaymath}

\subsubsection{Set equality}\index{set!equality}
Normally a set is unordered, which means that two sets that have their
members ordered in a different way, but consists of the same members are
equal. An example:

\begin{displaymath}
  \left\{1, 2, 3\right\} = \left\{1, 3, 2\right\} 
\end{displaymath}

\subsubsection{Subset}\index{set!subset}
Sets are often partially equal. That is, they are partly made up of parts
that are present in other sets. Two situations arise: they can either
contain objects that all are present in some other set, or they can
contain objects that are present in some other set and then some objects
which are not present int the other set. These situations are called
subset and proper subset respectively.

Two examples will make the distinction clear:

\begin{displaymath}
  \left\{1, 2, 3\right\} \subseteq \left\{1, 2, 3, 4, 5\right\}
\end{displaymath}

The above depicts a proper subset relation.

\begin{displaymath}
  \left\{1, 2, 3, a, b, c\right\} \subset \left\{1, 2, 3, 4, 5\right\}
\end{displaymath}

The above depicts a subset relation.

\subsubsection{Difference}\index{set!difference}
Different sets may describe different groups of objects, which
implicates that their set of members differ. To express the set of
objects that forms the set of difference between two sets, the
difference operator is used. The following examples should make the
semantics clear:

\begin{displaymath}
  \left\{ 1, 2, 3, a, b, c\right\} \backslash
  \left\{q\right\}
  = \left\{ 1, 2, 3, a, b, c\right\}
\end{displaymath}

\begin{displaymath}
  \left\{ 1, 2, 3, a, b, c\right\} \backslash
  \left\{1, 2, 3, a, b\right\}
  = \left\{ c \right\}
\end{displaymath}

\begin{displaymath}
  \left\{ 1, 2, 3, a, b, c\right\} \backslash
  \left\{1, 2, 3, a, b, c\right\}
  = \left\{ \right\} = \varnothing
\end{displaymath}

Where $\varnothing$ is the empty set.

%
\subsection{Powerset}\index{set!powerset}
A powerset describes all the possible ways to combinate the members of a
set. As such, the powerset function maps a set to a collection of all
subsets that belong to the original set. An example will clearify
how the mapping works:

\begin{displaymath}
  \wp(\left\{a,b,c\right\}) = 
    \left\{
        \varnothing, 
        \left\{ a \right\},
        \left\{ b \right\},
        \left\{ c \right\},
        \left\{ a, b \right\},
        \left\{ a, c\right\},
        \left\{ b, c\right\},
        \left\{ a, b, c\right\}
    \right\}
\end{displaymath}
Note how the set equality makes the number of sets lesser than if the
order of the elements in a set would matter.


%
\subsection{Lattices}\index{set!lattice} \index{lattice}
Lattices are a very important type of ordered sets, where an ordered set
is a set in which the set's members are internally ordered under some
relation. Lattices commonly occurs in traditional security theory, and will
be shortly revisited in the chapter on \texttt{security policies}.

A lattice is a structure which has both a single upper and lower bound,
and all other objects can be ordered using some relation between these
two.
For example, assume that the upper bound is the set: 
$\left\{ 1, 2, 3, a, b, c\right\}$, and the lower bound is the set:
$\left\{ a \right\}$. 
Figure~\ref{lattice} shows a resulting lattice under the relation
$\subseteq$.

\begin{figure}[!htpb]
\begin{center}
\includegraphics[height=70mm]{images/lattice.png}

\caption{A lattice of a few sets under the relation $\subseteq$}
\label{lattice}
\end{center}
\end{figure}
